Modal Companionを用いた決定可能性の証明